package com.googlecode.kipler.satisfiability.completion.branching;

import com.googlecode.kipler.container.dl.BasicWcsInterpolationData;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.satisfiability.interpolation.rule.FlatTracingInterpolantCalculation;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;

/**
 * 
 * @author İnanç Seylan
 * 
 */
public class LinearBranchingPoint extends BranchingPoint {
	private int accessCount;

	public LinearBranchingPoint(WorldConstraintSystem wcs) {
		setWcs(wcs);
	}

	@Override
	public boolean isBranchingPossible() {
		return getWcs() != null && accessCount == 0;
	}

	@Override
	public WorldConstraintSystem nextBranch() throws UnsatisfiableException {
		WorldConstraintSystem result = null;
		if (isBranchingPossible()) {
			accessCount++;
			result = getWcs();
		}
		return result;
	}

	@Override
	public void backtrack() {
		if (getWcs().getReasoner().getProfile().isInterpolationEnabled()) {
			BasicWcsInterpolationData data = (BasicWcsInterpolationData) getWcs()
					.getData();
			FlatTracingInterpolantCalculation iCalculator = new FlatTracingInterpolantCalculation();
			iCalculator.setPreviousInterpolant(data.getInterpolant());
			iCalculator.setWcs(getWcs());
			data.setInterpolant(iCalculator.apply());
		}
	}

}
